I have ErrorList docked at top, but not visible except when there are errors.
Auto-show on errors, auto-hide on no errors, auto-refocus on text area all selected
in errorlist options.
Whenever errorlist appears for the first time (after jEdit startup) it is pinned rather
than just docked normally.
If I unpin it in one session, it should not appear pinned next time I show it after
I re-run jEdit.
| Submitted | ezust - 2009-08-03 23:02:31 | Assigned | |
|---|---|---|---|
| Priority | 5 | Labels | |
| Status | open | Group | None |
| Resolution | None |
| 2009-08-04 03:13:31 *anonymous |
In general, you usually want your dockables pinned. Pinned means that they remain
visible if they lose focus. The 'auto hide' feature of error list is not related to
the "pinned" state, it uses the dockable window manager's hideDockable method (or
similar).
|
|---|